/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ¬⊂AI Applications of Circumscription

␈↓ α∧␈↓␈↓ αT(McCarthy␈α1980)␈αintroduces␈αthe␈α
circumscription␈αmethod␈αof␈αnon-monotonic␈α
reasoning.␈α The

␈↓ α∧␈↓paper␈αgives␈αmotivation,␈αsome␈αmathematical␈α
properties␈αand␈αsome␈αexamples␈αof␈αits␈α
application.␈α We

␈↓ α∧␈↓assume acquaintance with the ideas of that paper.

␈↓ α∧␈↓␈↓ αTThe␈α
present␈αpaper␈α
gives␈αa␈α
slightly␈α
generalized␈αform␈α
of␈αcircumscription␈α
and␈α
applications␈αto

␈↓ α∧␈↓representing␈αcommon␈αsense␈αfacts␈αin␈αa␈αdata␈αbase.␈α It␈αturns␈αout␈αthat␈αmany␈αsuch␈αapplications␈αcan␈αbe

␈↓ α∧␈↓done␈αin␈αa␈αuniform␈αway.␈α A␈αsingle␈αpredicate␈α␈↓↓ab,␈↓␈αstanding␈αfor␈α"abnormal"␈αis␈αcircumscribed␈αwith␈αall

␈↓ α∧␈↓other␈α⊂predicates␈α⊂and␈α⊂functions␈α⊂considered␈α⊂as␈α∂variables␈α⊂that␈α⊂can␈α⊂be␈α⊂constrained␈α⊂to␈α⊂achieve␈α∂the

␈↓ α∧␈↓circumscription␈α∞subject␈α∞to␈α∞the␈α∞axioms.␈α∞ Whether␈α∞other␈α∞applications␈α∞require␈α∞circumscribing␈α
other

␈↓ α∧␈↓formulas than ␈↓↓ab z␈↓ is presently unknown.

␈↓ α∧␈↓␈↓ αTWe begin with our generalized circumscription

␈↓ α∧␈↓␈↓αDefinition:␈↓␈α∞Let␈α∞␈↓↓A(P)␈↓␈α∞be␈α∞a␈α∞formula␈α∞of␈α∂second␈α∞order␈α∞logic␈α∞involving␈α∞a␈α∞tuple␈α∞␈↓↓P␈↓␈α∞of␈α∂free␈α∞predicate

␈↓ α∧␈↓symbols.␈α Let␈α␈↓↓E(P,x)␈↓␈αbe␈αa␈αwff␈αin␈αwhich␈α␈↓↓P␈↓␈αand␈αa␈αtuple␈α␈↓↓x␈↓␈αof␈αindividual␈αvariables␈αoccur␈αfree.␈α The

␈↓ α∧␈↓circumscription of ␈↓↓E(P,x)␈↓ relative to ␈↓↓A(P)␈↓ is the formula ␈↓↓A'(P)␈↓ defined by

␈↓ α∧␈↓1)␈↓ αt ␈↓↓A(P) ∧ ∀P'.[A(P') ∧ [∀x.E(P',x) ⊃ E(P,x)] ⊃ [∀x.E(P',x) ≡ E(P,x)]].␈↓

␈↓ α∧␈↓[We␈α∞are␈α∞here␈α∞writing␈α
␈↓↓A(P)␈↓␈α∞instead␈α∞of␈α∞␈↓↓A(P␈↓β1␈↓↓, . . . ,P␈↓βn␈↓↓)␈↓␈α
for␈α∞brevity␈α∞and␈α∞likewise␈α∞writing␈α
␈↓↓E(P,x)␈↓

␈↓ α∧␈↓instead␈α
of␈α␈↓↓E(P␈↓β1␈↓↓, . . . ,P␈↓βn␈↓↓,x␈↓β1␈↓↓, . . . ,x␈↓βn␈↓↓)␈↓.␈α
 Likewise␈αthe␈α
quantifier␈α
␈↓↓∀x␈↓␈αstands␈α
for␈α␈↓↓∀x␈↓β1␈↓↓ . . . x␈↓βn␈↓.␈α
 We

␈↓ α∧␈↓don't use the full generality in this paper.

␈↓ α∧␈↓␈↓ αTThere␈α
are␈αtwo␈α
differences␈α
between␈αthis␈α
and␈α(McCarthy␈α
1980).␈α
 First,␈αin␈α
that␈α
paper␈α␈↓↓E(P,x)␈↓

␈↓ α∧␈↓had␈α⊂the␈α⊂specific␈α⊂form␈α⊂␈↓↓P(x).␈↓␈α∂Here␈α⊂we␈α⊂speak␈α⊂of␈α⊂circumscribing␈α∂a␈α⊂wff,␈α⊂while␈α⊂there␈α⊂we␈α⊂spoke␈α∂of

␈↓ α∧␈↓circumscribing␈αa␈αpredicate.␈α Second,␈αin␈α(1)␈αwe␈αuse␈αan␈αexplicit␈αquantifier␈αfor␈αthe␈αpredicate␈αvariable

␈↓ α∧␈↓␈↓↓P'␈↓␈α⊃whereas␈α∩in␈α⊃(McCarthy␈α⊃1980),␈α∩the␈α⊃formula␈α⊃was␈α∩a␈α⊃schema.␈α⊃ The␈α∩advantage␈α⊃of␈α∩the␈α⊃present

␈↓ α∧␈↓formalism␈αis␈αthat␈αnow␈α␈↓↓A'(P)␈↓␈αis␈αthe␈αsame␈αkind␈αof␈αentity␈αas␈α␈↓↓A(P)␈↓␈αand␈αcan␈αbe␈αused␈αas␈αthe␈αaxiom␈αfor

␈↓ α∧␈↓circumscribing some other wff.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓1. Minimizing abnormality

␈↓ α∧␈↓␈↓ αTMany␈α⊂people␈α⊂have␈α⊂imagined␈α⊂representing␈α⊂facts␈α∂about␈α⊂what␈α⊂is␈α⊂"normally"␈α⊂the␈α⊂case.␈α∂ One

␈↓ α∧␈↓problem␈αis␈αthat␈αevery␈αobject␈αis␈αabnormal␈αin␈αsome␈αway,␈αand␈αwe␈αwant␈αto␈αallow␈αsome␈αaspects␈αof␈αthe

␈↓ α∧␈↓object␈αto␈αbe␈α
abnormal␈αand␈αstill␈α
conclude␈αthe␈αnormality␈α
of␈αthe␈αrest.␈α
 We␈αdo␈αthis␈α
with␈αa␈αpredicate␈α
␈↓↓ab␈↓

␈↓ α∧␈↓standing␈α
for␈α"abnormal".␈α
 We␈αcircumscribe␈α
␈↓↓ab x␈↓.␈α The␈α
argument␈αof␈α
␈↓↓ab␈↓␈αwill␈α
be␈αsome␈α
aspect␈α
of␈αthe

␈↓ α∧␈↓entities␈α
involved.␈α Some␈α
aspects␈α
can␈αbe␈α
abnormal␈α
without␈αaffecting␈α
others.␈α
 The␈αaspects␈α
themselves

␈↓ α∧␈↓are␈αabstract␈αentities,␈αand␈αtheir␈αunfamiliarity␈αis␈αsomewhat␈αa␈αblemish␈αon␈αthe␈αtheory.␈α Next␈αwe␈αhave

␈↓ α∧␈↓applications.



␈↓ α∧␈↓2. The unique names hypothesis

␈↓ α∧␈↓␈↓ αTRaymond␈α→Reiter␈α→(1979)␈α→introduced␈α→the␈α→phrase␈α→"unique␈α→names␈α→hypothesis"␈α~for␈α→the

␈↓ α∧␈↓assumption␈αthat␈αdistinct␈αnames␈αdenote␈αdistinct␈αobjects.␈α We␈αwant␈αto␈αshow␈αhow␈αto␈αhandle␈αthis␈αin␈αa

␈↓ α∧␈↓more general way by circumscription.

␈↓ α∧␈↓␈↓ αTSuppose␈α
we␈α
introduce␈α
names␈α
as␈α
objects,␈α
i.e.␈α
we␈α
introduce␈α
␈↓↓'John␈↓␈α
as␈α
a␈α
name␈α
for␈α∞John.␈α
 For

␈↓ α∧␈↓brevity␈α∞we␈α
use␈α∞the␈α
Lisp␈α∞notation␈α
␈↓↓'John␈↓␈α∞instead␈α
of␈α∞the␈α
more␈α∞usual␈α
"John".␈α∞ We␈α
then␈α∞assume␈α
an

␈↓ α∧␈↓infinity of first order axioms like

␈↓ α∧␈↓␈↓ αT␈↓↓'John ≠ 'Henry␈↓,

␈↓ α∧␈↓i.e.␈α∪for␈α∪every␈α∀pair␈α∪of␈α∪distinct␈α∀names␈α∪there␈α∪is␈α∪such␈α∀an␈α∪axiom.␈α∪ From␈α∀the␈α∪point␈α∪of␈α∀view␈α∪of

␈↓ α∧␈↓mathematical␈α⊗logic,␈α↔there␈α⊗is␈α↔no␈α⊗harm␈α↔in␈α⊗having␈α⊗an␈α↔infinity␈α⊗of␈α↔such␈α⊗axioms.␈α↔ From␈α⊗the

␈↓ α∧␈↓computational␈α∩point␈α∪of␈α∩view␈α∩of␈α∪a␈α∩theorem␈α∪proving␈α∩or␈α∩problem␈α∪solving␈α∩program,␈α∪we␈α∩merely

␈↓ α∧␈↓suppose␈α∩that␈α⊃we␈α∩rely␈α∩on␈α⊃the␈α∩computer␈α⊃to␈α∩generate␈α∩the␈α⊃assertion␈α∩that␈α⊃two␈α∩names␈α∩are␈α⊃distinct

␈↓ α∧␈↓whenever␈αthis␈αis␈α
required,␈αsince␈αa␈α
subroutine␈αcan␈αeasily␈α
tell␈αwhether␈αtwo␈α
strings␈αare␈αthe␈αsame.␈α
 We

␈↓ α∧␈↓might␈α
suppose␈αthat␈α
some␈α
metamathematical␈αconsiderations␈α
would␈α
change␈αfrom␈α
using␈α
an␈αinfinity␈α
of

␈↓ α∧␈↓axioms,␈α∂but␈α∂usually␈α⊂this␈α∂won't␈α∂be␈α∂so,␈α⊂because␈α∂we␈α∂can␈α∂generate␈α⊂an␈α∂infinity␈α∂of␈α⊂provably␈α∂distinct
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓objects␈α
from␈α
a␈α
finite␈α
set␈α
of␈α
axioms.␈α
 All␈α
we␈α
need␈α
do␈α
is␈α
use␈α
integers␈α
as␈α
names,␈α
axiomatize␈α
>␈α
as␈α
a

␈↓ α∧␈↓relation␈αincluding␈αits␈αtransitivity␈α
and␈αhave␈αan␈αaxiom␈α
␈↓↓∀x y.x > y ⊃ x ≠ y␈↓.␈α It␈αis␈αequally␈α
feasible␈αto

␈↓ α∧␈↓finitely axiomatize strings in a way that ensures that distinct strings are provably distinct.

␈↓ α∧␈↓␈↓ αTOne way of getting unique names is to use axioms like

␈↓ α∧␈↓2)␈↓ αt ␈↓↓name(John) = 'John␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓name(Henry) = 'Henry␈↓.

␈↓ α∧␈↓The distinctness of names and the theory of inequality will then give ␈↓↓John ≠ Henry␈↓.

␈↓ α∧␈↓␈↓ αTHowever,␈α⊂this␈α⊃is␈α⊂too␈α⊃absolute␈α⊂for␈α⊃many␈α⊂applications.␈α⊃ It␈α⊂is␈α⊃often␈α⊂preferable␈α⊃that␈α⊂objects

␈↓ α∧␈↓denoted␈αby␈αdistinct␈αnames␈αare␈αto␈αbe␈αpresumed␈αdistinct␈αunless␈αthere␈αis␈αreason␈αto␈αbelieve␈αthem␈αto␈αbe

␈↓ α∧␈↓the same.  We can do this as follows.  Instead of using axioms like (2), we write

␈↓ α∧␈↓3)␈↓ αt ␈↓↓denotation('John) = John␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓denotation('Henry) = Henry␈↓

␈↓ α∧␈↓Nothing now prevents ␈↓↓John = Henry␈↓, so we use the axiom

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀n1 n2. n1 ≠ n2 ∧ ¬ab aspecteq(n1,n2) ⊃ denotation n1 ≠ denotation n2␈↓.

␈↓ α∧␈↓␈↓ αTThe␈αidea␈αof␈αthis␈αaxiom␈αis␈αthat␈αif␈α␈↓↓n1␈↓␈αand␈α␈↓↓n2␈↓␈αare␈αdistinct␈αnames,␈αand␈α␈↓↓aspecteq(n1,n2)␈↓␈αis␈αnot

␈↓ α∧␈↓abnormal,␈αi.e.␈αdoes␈αnot␈αsatisfy␈αthe␈αpredicate␈α␈↓↓ab,␈↓␈αthen␈α␈↓↓n1␈↓␈αand␈α␈↓↓n2␈↓␈αdenote␈αdistinct␈αobjects.␈α When␈α
we

␈↓ α∧␈↓have␈α"taken␈αinto␈αaccount"␈αall␈αthe␈αfacts␈αwe␈αare␈αgoing␈αto␈αtake␈αinto␈αaccount␈αwe␈αwill␈αcircumscribe␈αthe

␈↓ α∧␈↓expression␈α
␈↓↓ab x␈↓.␈α
 This␈α
will␈α
make␈α
␈↓↓ab aspecteq(n1,n2)␈↓␈α
false␈α
unless␈α
some␈α
facts␈α
prevent␈α
it␈α
and␈α
hence

␈↓ α∧␈↓will␈αallow␈αinferring␈αthat␈α␈↓↓denotation n1␈↓␈αand␈α␈↓↓denotation n2␈↓␈αdistinct␈αif␈αthere␈αis␈αno␈αevidence␈αthat␈αthey

␈↓ α∧␈↓are equal.


␈↓ α∧␈↓3. Some other examples of Reiter

␈↓ α∧␈↓␈↓ αTReiter␈α∃asks␈α∃about␈α∃representing,␈α∃"Quakers␈α∀are␈α∃normally␈α∃pacifists␈α∃and␈α∃Republicans␈α∀are

␈↓ α∧␈↓normally non-pacificists.  How about Nixon, who is both a Quaker and a Republican?"
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓We use

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀x.quaker x ∧ ¬ab aspect1 x ⊃ pacifist x␈↓,

␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀x.republican x ∧ ¬ab aspect2 x ⊃ ¬ pacifist x␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓7)␈↓ αt ␈↓↓quaker Nixon ∧ pacifist Nixon␈↓.

␈↓ α∧␈↓␈↓ αTWhen␈α∞we␈α∞circumscribe␈α∂␈↓↓ab z␈↓␈α∞using␈α∞these␈α∞three␈α∂sentences␈α∞as␈α∞␈↓↓A(ab),␈↓␈α∞we␈α∂will␈α∞only␈α∞be␈α∂able␈α∞to

␈↓ α∧␈↓conclude␈αthat␈αNixon␈αis␈α
either␈αabnormal␈αin␈α␈↓↓aspect1␈↓␈α
or␈αin␈α␈↓↓aspect2,␈↓␈αand␈αwe␈α
will␈αnot␈αbe␈αable␈α
to␈αsay

␈↓ α∧␈↓whether he is a pacifist.

␈↓ α∧␈↓␈↓ αTThe␈αsecond␈αexample␈αis␈αthat␈αa␈αperson␈αnormally␈αlives␈αin␈αthe␈αsame␈αcity␈αas␈αhis␈αwife␈αand␈αin␈αthe

␈↓ α∧␈↓same city as his employer.  But A



␈↓ α∧␈↓4. Whether birds can fly

␈↓ α∧␈↓␈↓ αTI␈αhave␈αexplored␈αmany␈αways␈αof␈αnon-monotonically␈αaxiomatizing␈αthe␈αfacts␈αabout␈αwhich␈αbirds

␈↓ α∧␈↓can fly.  The following axioms using ␈↓↓ab␈↓ seems to me quite straightforward.

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.  Unless an object is abnormal in ␈↓↓aspect1,␈↓ it can't fly.

␈↓ α∧␈↓␈↓ αTNote␈α
that␈α
it␈α
wouldn't␈α
work␈α
to␈α
write␈α
␈↓↓ab␈α
x␈↓␈α
instead␈α
of␈α
␈↓↓ab␈α
aspect1␈α
x␈↓,␈α
because␈α
we␈α
don't␈α∞want␈α
a

␈↓ α∧␈↓bird␈α⊂that␈α⊂is␈α⊂abnormal␈α⊂with␈α⊂respect␈α⊂to␈α⊂its␈α⊂ability␈α⊂to␈α⊂fly␈α⊂to␈α⊂be␈α⊂automatically␈α⊂abnormal␈α⊂in␈α⊂other

␈↓ α∧␈↓respects.  Using aspects limits the effects of proofs of abnormality.

␈↓ α∧␈↓9)␈↓ αt␈α␈↓↓∀x.bird␈αx␈α⊃␈αab␈αaspect1␈αx␈↓.␈α A␈αbird␈αis␈αabnormal␈αin␈αaspect1,␈αso␈α(8)␈αcan't␈αbe␈αused␈αto␈αshow␈αit

␈↓ α∧␈↓can't␈αfly.␈α If␈αthis␈αaxiom␈αwere␈αomitted,␈αwhen␈α
we␈αdid␈αthe␈αcircumscription␈αwe␈αwould␈αonly␈αbe␈α
able␈αto

␈↓ α∧␈↓infer␈α∞a␈α
disjunction.␈α∞ Either␈α∞a␈α
bird␈α∞is␈α
abnormal␈α∞in␈α∞aspect1␈α
or␈α∞it␈α
can␈α∞fly␈α∞unless␈α
it␈α∞is␈α∞abnormal␈α
in

␈↓ α∧␈↓aspect2.␈α (9)␈α
establishes␈αexpresses␈α
our␈αpreference␈α
for␈αinferring␈αthat␈α
a␈αbird␈α
is␈αabnormal␈α
in␈αaspect1

␈↓ α∧␈↓rather than aspect2.

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.  Unless a bird is abnormal in aspect2, it can fly.
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓11)␈↓ αt␈α
␈↓↓∀x.ostrich␈α∞x␈α
⊃␈α∞ab␈α
aspect2␈α
x␈↓.␈α∞ Ostriches␈α
are␈α∞abnormal␈α
in␈α
aspect2.␈α∞ This␈α
doesn't␈α∞say␈α
that

␈↓ α∧␈↓ostriches cannot fly - merely that (10) can't be used to infer that it does.

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀x.penguin x ⊃ ab aspect2 x␈↓.  Penguins are also abnormal in aspect2.

␈↓ α∧␈↓13)␈↓ αt ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓14)␈↓ αt ␈↓↓∀x.penguin x ∧¬ab aspect4 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓Normally␈αostriches␈α
and␈αpenguins␈αcan't␈α
fly.␈α However,␈αthere␈α
is␈αan␈αout.␈α
 (13)␈αand␈α(14)␈α
provide␈αthat

␈↓ α∧␈↓under␈α⊃unspecified␈α⊃conditions,␈α⊃an␈α⊃ostrich␈α⊃or␈α⊃penguin␈α⊃might␈α⊃fly␈α⊃after␈α⊃all.␈α⊃ If␈α⊃we␈α⊃give␈α∩no␈α⊃such

␈↓ α∧␈↓conditions,␈αwe␈α
will␈αconclude␈α
that␈αan␈α
ostrich␈αor␈α
penguin␈αcan't␈α
fly.␈α Additional␈α
objects␈αthat␈α
can␈αfly

␈↓ α∧␈↓may␈α∂be␈α∂specified.␈α⊂ Each␈α∂needs␈α∂two␈α⊂axioms.␈α∂ The␈α∂first␈α⊂says␈α∂that␈α∂it␈α⊂is␈α∂abnormal␈α∂in␈α⊂aspect1␈α∂and

␈↓ α∧␈↓prevents␈α(3)␈αfrom␈αbeing␈αused␈αto␈αsay␈αthat␈αit␈αcan't␈αfly.␈α The␈αsecond␈αprovides␈αthat␈αit␈αcan␈αfly␈αunless␈αit

␈↓ α∧␈↓is abnormal in yet another way.  Likewise additional non-flying birds can be provided for.

␈↓ α∧␈↓␈↓ αTWe␈α
haven't␈αyet␈α
said␈αthat␈α
ostriches␈αand␈α
penguins␈αare␈α
birds,␈αso␈α
let's␈αdo␈α
that␈αand␈α
throw␈αin␈α
that

␈↓ α∧␈↓canaries are birds also.

␈↓ α∧␈↓15)␈↓ αt ␈↓↓∀x.ostrich x ⊃ bird x␈↓

␈↓ α∧␈↓16)␈↓ αt ␈↓↓∀x.penguin x ⊃ bird x␈↓

␈↓ α∧␈↓17)␈↓ αt␈α␈↓↓∀x.canary␈α
x␈α∧␈α
¬ab␈αaspect5␈α
x␈α⊃␈α
bird␈αx␈↓␈α
We␈αthrew␈α
in␈α␈↓↓aspect5␈↓␈α
just␈αin␈α
case␈αone␈α
wanted␈αto␈α
use

␈↓ α∧␈↓the term canary in the sense of a 1930s gangster movie.

␈↓ α∧␈↓Asserting␈α
that␈α
ostriches,␈α
penguins␈α
and␈α
canaries␈α∞are␈α
birds␈α
will␈α
help␈α
inherit␈α
other␈α∞properties␈α
from

␈↓ α∧␈↓the class of birds.  For example, we have

␈↓ α∧␈↓18)␈↓ αt ␈↓↓∀x. bird x ∧ ¬ab aspect6 x ⊃ feathered x␈↓.

␈↓ α∧␈↓So␈αfar␈αthere␈α
is␈αnothing␈αto␈α
prevent␈αostriches,␈αpenguins␈αand␈α
canaries␈αfrom␈αoverlapping.␈α
 We␈αcould

␈↓ α∧␈↓write disjointness axioms like

␈↓ α∧␈↓19)␈↓ αt␈↓↓∀x. ¬ostrich x ∨ ¬penguin x␈↓,

␈↓ α∧␈↓but␈αwe␈αwould␈αrequire␈α␈↓↓n␈↓∧2␈↓␈αof␈αthem␈αif␈αwe␈αhave␈α␈↓↓n␈↓␈αspecies.␈α We␈αneed␈αto␈αdo␈αsomething␈αlike␈αthe␈αunique

␈↓ α∧␈↓names circumscription again.
␈↓ α∧␈↓␈↓ u6


␈↓ α∧␈↓Therefore, we write axioms

␈↓ α∧␈↓20)␈↓ αt ␈↓↓∀x. ostrich x ≡ belongs(x,'ostrich)␈↓

␈↓ α∧␈↓and similarly for penguins, canaries and birds.  We can now write

␈↓ α∧␈↓21)␈↓ αt ␈↓↓∀n1 n2. n1 ≠ n2 ∧ ¬ab aspect8(n1,n2) ⊃ ∀x.¬(belongs(x,n1) ∧ belongs(x,n2)␈↓.

␈↓ α∧␈↓This␈αdoesn't␈αdo␈α
everything␈αwe␈αwant,␈αbecause␈α
we␈αhave␈αallowed␈α
a␈αcanary␈α␈↓↓x␈↓␈αtwo␈α
choices.␈α It␈αcan␈αbe␈α
a

␈↓ α∧␈↓bird␈αavoiding␈α␈↓↓ab aspect5 x␈↓␈αor␈αit␈αcan␈αbe␈αa␈αnon-bird␈αavoiding␈α␈↓↓aspect8('canary,'bird)␈↓.␈α We␈αwant␈α
the

␈↓ α∧␈↓former to have priority and can do it simply by writing

␈↓ α∧␈↓22)␈↓ αt ␈↓↓ab aspect8('canary,bird)␈↓.

␈↓ α∧␈↓␈↓ αTIn␈αwhat␈αfollows␈αwe␈αwill␈αneed␈αuniqueness␈αaxioms␈αfor␈αthe␈αaspects,␈αand␈αthey␈αare␈αa␈αnuisance␈αto

␈↓ α∧␈↓write.  They could be written

␈↓ α∧␈↓23)␈↓ αt␈↓↓∀n1 n2 x1 x2.aspect(n1,x1) = aspect(n2,x2) ≡ n1 = n2 ∧ x1 = x2␈↓,

␈↓ α∧␈↓if␈α∂we␈α∂make␈α∞␈↓↓n␈↓␈α∂a␈α∂parameter,␈α∞i.e.␈α∂write␈α∂␈↓↓aspect(2,x)␈↓␈α∞instead␈α∂of␈α∂␈↓↓aspect2 x,␈↓␈α∞but␈α∂even␈α∂this␈α∂doesn't␈α∞to

␈↓ α∧␈↓everything␈α∞we␈α∞need,␈α∞because␈α∞it␈α∞doesn't␈α∞cover␈α∞aspects␈α∞that␈α∞take␈α∞more␈α∞than␈α∞one␈α∂argument.␈α∞ Many

␈↓ α∧␈↓argument␈αaspects␈αcan␈αbe␈αreduced␈αto␈αone␈αargument␈αaspects␈αby␈αassuming␈αthem␈αto␈αoperate␈αon␈αtuples.

␈↓ α∧␈↓For␈α∂this␈α∂paper,␈α∞we␈α∂won't␈α∂make␈α∞this␈α∂change␈α∂of␈α∞notation␈α∂and␈α∂merely␈α∞assume␈α∂that␈α∂all␈α∂aspects␈α∞are

␈↓ α∧␈↓distinct objects.



␈↓ α∧␈↓5. General considerations

␈↓ α∧␈↓␈↓ αTSuppose␈αwe␈α
have␈αa␈αdata␈α
base␈αof␈αfacts␈α
axiomatized␈αby␈αa␈α
formalism␈αinvolving␈α
the␈αpredicate

␈↓ α∧␈↓␈↓↓ab.␈↓␈α∩In␈α∩connection␈α∩with␈α∩a␈α∩particular␈α∩problem,␈α∩a␈α∩program␈α∩takes␈α∩a␈α∩subcollection␈α∩of␈α∩these␈α⊃facts

␈↓ α∧␈↓together␈αwith␈αthe␈αspecific␈αfacts␈αof␈αthe␈αproblem␈α
and␈αthe␈αcircumscribes␈α␈↓↓ab␈↓␈αx.␈α We␈αget␈αa␈αsecond␈α
order

␈↓ α∧␈↓formula,␈αand␈αin␈αgeneral,␈αas␈αthe␈αnatural␈αnumber␈αexample␈αof␈α(McCarthy␈α1980)␈αshows,␈αthis␈αformula

␈↓ α∧␈↓is␈α∀not␈α∀equivalent␈α∀to␈α∃any␈α∀first␈α∀order␈α∀formula.␈α∃ However,␈α∀many␈α∀common␈α∀sense␈α∃domains␈α∀are

␈↓ α∧␈↓axiomatizable␈αin␈α
such␈αa␈α
way␈αthat␈αthe␈α
circumscription␈αis␈α
equivalent␈αto␈αa␈α
first␈αorder␈α
formula.␈α For
␈↓ α∧␈↓␈↓ u7


␈↓ α∧␈↓example,␈α⊂Vladimir␈α⊂Lifschitz␈α⊂(1983)␈α⊂has␈α⊂shown␈α⊂that␈α∂this␈α⊂is␈α⊂true␈α⊂if␈α⊂the␈α⊂axioms␈α⊂are␈α⊂a␈α∂universal

␈↓ α∧␈↓formula␈α⊂and␈α⊂there␈α∂are␈α⊂no␈α⊂functions.␈α∂ This␈α⊂can␈α⊂presumably␈α∂be␈α⊂extended␈α⊂to␈α∂the␈α⊂case␈α⊂when␈α∂the

␈↓ α∧␈↓ranges␈αand␈α
domains␈αof␈α
the␈αfunctions␈αare␈α
disjoint,␈αso␈α
that␈αthere␈αis␈α
no␈αway␈α
of␈αgenerating␈αan␈α
infinity

␈↓ α∧␈↓of elements.

␈↓ α∧␈↓␈↓ αTWe␈α⊃can␈α⊃then␈α⊃regard␈α⊃the␈α⊃process␈α⊃of␈α⊃deciding␈α⊃what␈α⊃facts␈α⊃to␈α⊃take␈α⊃into␈α⊃account␈α⊃and␈α⊂then

␈↓ α∧␈↓circumscribing␈α
as␈α
a␈αprocess␈α
of␈α
compiling␈αfrom␈α
a␈α
slightly␈αhigher␈α
level␈α
non-monotonic␈αlanguage␈α
into

␈↓ α∧␈↓mathematical␈α∞logic,␈α∂especially␈α∞first␈α∂order␈α∞logic.␈α∂ We␈α∞can␈α∂also␈α∞regard␈α∂natural␈α∞language␈α∂as␈α∞higher

␈↓ α∧␈↓level␈α∃than␈α∃logic,␈α∃although,␈α∃as␈α∃I␈α∃shall␈α∃discuss␈α∃elsewhere,␈α∃natural␈α∃language␈α∃doesn't␈α∃have␈α∀an

␈↓ α∧␈↓independent␈α∪reasoning␈α∪process,␈α∪because␈α∪most␈α∪natural␈α∪language␈α∪inferences␈α∀involve␈α∪suppressed

␈↓ α∧␈↓premisses␈α∞which␈α∞are␈α∞not␈α∂represented␈α∞in␈α∞natural␈α∞language␈α∞in␈α∂the␈α∞minds␈α∞of␈α∞the␈α∞people␈α∂doing␈α∞the

␈↓ α∧␈↓reasoning.



␈↓ α∧␈↓6. An example of doing the circumscription.

␈↓ α∧␈↓␈↓ αTIn␈αorder␈αto␈αkeep␈αthe␈α
example␈αshort␈αwe␈αwill␈αtake␈α
into␈αaccount␈αonly␈αthe␈αfollowing␈α
facts␈αfrom

␈↓ α∧␈↓the previous section.

␈↓ α∧␈↓8) ␈↓↓∀x.¬ab aspect1 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓9) ␈↓↓∀x.bird x ⊃ ab aspect1 x␈↓.

␈↓ α∧␈↓10) ␈↓↓∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x␈↓.

␈↓ α∧␈↓11) ␈↓↓∀x.ostrich x ⊃ ab aspect2 x␈↓.

␈↓ α∧␈↓13) ␈↓↓∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x␈↓.

␈↓ α∧␈↓␈↓ αTTheir conjunction is taken as ␈↓↓A(ab,flies)␈↓.  The circumscription formula ␈↓↓A'(ab,flies)␈↓ is then

␈↓ α∧␈↓24)␈↓ αt ␈↓↓A(ab,flies) ∧ ∀ab' flies'.[A(ab',flies') ∧ [∀x. ab' x ⊃ ab x] ⊃ [∀x. ab x ≡ ab' x]]␈↓,

␈↓ α∧␈↓which spelled out becomes

␈↓ α∧␈↓25)␈↓ αt␈α␈↓↓[∀x.¬ab␈α
aspect1␈αx␈α
⊃␈α¬flies␈αx]␈α
∧␈α[∀x.bird␈α
x␈α⊃␈α
ab␈αaspect1␈αx]␈α
∧␈α[∀x.bird␈α
x␈α∧␈α
¬ab␈αaspect2␈αx␈α
⊃
␈↓ α∧␈↓␈↓ u8


␈↓ α∧␈↓↓flies␈α⊃x]␈α⊃∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃⊃␈α⊃ab␈α⊃aspect2␈α⊃x]␈α∩∧␈α⊃[∀x.ostrich␈α⊃x␈α⊃∧␈α⊃¬ab␈α⊃aspect3␈α⊃x␈α⊃⊃␈α⊃¬flies␈α⊃x]␈α∩∧␈α⊃∀ab'

␈↓ α∧␈↓↓flies'.[[∀x.¬ab'␈αaspect1␈αx␈α⊃␈α¬flies'␈αx]␈α∧␈α[∀x.bird␈αx␈α⊃␈αab'␈αaspect1␈αx]␈α∧␈α[∀x.bird␈αx␈α∧␈α¬ab'␈αaspect2␈αx

␈↓ α∧␈↓↓⊃␈α
flies'␈α
x]␈α
∧␈α
[∀x.ostrich␈α
x␈α
⊃␈α
ab'␈α
aspect2␈α
x]␈α
∧␈α
[∀x.ostrich␈α
x␈α
∧␈α
¬ab'␈α
aspect3␈α
x␈α
⊃␈α
¬flies'␈α
x]␈α
∧␈α
[∀x.ab'␈α
x

␈↓ α∧␈↓↓⊃ ab x] ⊃ [∀x.ab x ≡ ab' x]]␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓A(ab,flies)␈↓␈α
is␈α
guaranteed␈α
to␈α
be␈α
true,␈α
because␈α
it␈α
is␈α
part␈α
of␈α
what␈α
is␈α
assumed␈α
in␈α
our␈αcommon

␈↓ α∧␈↓sense data base.  Therfore (25) reduces to

␈↓ α∧␈↓26)␈↓ αt␈↓↓∀ab'␈αflies'.[[∀x.¬ab'␈αaspect1␈α
x␈α⊃␈α¬flies'␈α
x]␈α∧␈α[∀x.bird␈αx␈α
⊃␈αab'␈αaspect1␈α
x]␈α∧␈α[∀x.bird␈α
x␈α∧

␈↓ α∧␈↓↓¬ab'␈α∂aspect2␈α∞x␈α∂⊃␈α∞flies'␈α∂x]␈α∞∧␈α∂[∀x.ostrich␈α∞x␈α∂⊃␈α∞ab'␈α∂aspect2␈α∞x]␈α∂∧␈α∞[∀x.ostrich␈α∂x␈α∞∧␈α∂¬ab'␈α∞aspect3␈α∂x␈α∞⊃

␈↓ α∧␈↓↓¬flies' x] ∧ [∀x.ab' x ⊃ ab x] ⊃ [∀x.ab x ≡ ab' x]]␈↓.

␈↓ α∧␈↓␈↓ αTOur␈α
objective␈αis␈α
now␈α
to␈αmake␈α
suitable␈α
substitutions␈αfor␈α
␈↓↓ab'␈↓␈αand␈α
flies'␈α
so␈αthat␈α
all␈α
the␈αterms

␈↓ α∧␈↓except␈αthe␈α
last␈αof␈α
(26)␈αwill␈α
be␈αtrue,␈αand␈α
the␈αlast␈α
term␈αwill␈α
determine␈α␈↓↓ab.␈↓␈α
The␈αaxiom␈α␈↓↓A(ab,flies)␈↓␈α
will

␈↓ α∧␈↓then␈α
determine␈α∞␈↓↓flies,␈↓␈α
i.e.␈α
we␈α∞will␈α
know␈α
what␈α∞the␈α
fliers␈α
are.␈α∞ ␈↓↓flies'␈↓␈α
is␈α
easy,␈α∞because␈α
we␈α∞need␈α
only

␈↓ α∧␈↓apply␈αwishful␈αthinking;␈αwe␈αwant␈αthe␈αfliers␈αto␈αjust␈αthose␈αbirds␈αthat␈αaren't␈αostriches.␈α Therefore,␈αwe

␈↓ α∧␈↓put

␈↓ α∧␈↓27)␈↓ αt ␈↓↓flies' x ≡ bird x ∧ ¬ostrich x␈↓.

␈↓ α∧␈↓␈↓ αT␈↓↓ab'␈↓ isn't really much more difficult, but there is a notational problem.  We define

␈↓ α∧␈↓28)␈↓ αt ␈↓↓ab' z ≡ [∃x.bird x ∧ z = aspect1 x] ∨ [∃x.ostrich x ∧ z = aspect2 x]␈↓,

␈↓ α∧␈↓which covers the cases we want to be abnormal.


␈↓ α∧␈↓7. The blocks world

␈↓ α∧␈↓␈↓ αTThe␈αfolowing␈αset␈αof␈α
"situation␈αcalculus"␈αaxioms␈αsolves␈αthe␈α
frame␈αproblem␈αfor␈αa␈αblocks␈α
world

␈↓ α∧␈↓in which blocks can be moved and painted.

␈↓ α∧␈↓29)␈↓ αt ␈↓↓∀x e s.¬ab aspect1(x,e,s) ⊃ location(x,result(e,s)) = location(x,s)␈↓.

␈↓ α∧␈↓30)␈↓ αt ␈↓↓∀x e s.¬ab aspect2(x,e,s) ⊃ color(x,result(e,s)) = color(x,s)␈↓.

␈↓ α∧␈↓Objects change their locations and colors only for a reason.

␈↓ α∧␈↓31)␈↓ αt ␈↓↓∀x l s.¬ab aspect3(x,l,s) ⊃ ab aspect1(x,move(x,l),s)␈↓
␈↓ α∧␈↓␈↓ u9


␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x l s.¬ab aspect3(x,l,s) ⊃ location(x,result(move(x,l),s)) = l␈↓.

␈↓ α∧␈↓32)␈↓ αt ␈↓↓∀x c s.¬ab aspect4(x,c,s) ⊃ ab aspect2(x,paint(x,c),s)␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x c s.¬ab aspect4(x,c,s) ⊃ color(x,result(paint(x,c),s)) = c␈↓.

␈↓ α∧␈↓Objects change their locations when moved and their colors when painted.

␈↓ α∧␈↓33)␈↓ αt ␈↓↓∀x l s.¬clear(top x,s) ∨ ¬clear(l,s) ∨ tooheavy x ⊃ ab aspect3(x,move(x,l),s)␈↓.

␈↓ α∧␈↓This␈αprevents␈αthe␈αrule␈α(31)␈αfrom␈αbeing␈αused␈αto␈αinfer␈αthat␈αan␈αobject␈αwill␈αmove␈αif␈αit␈αisn't␈αclear␈αor␈α
to

␈↓ α∧␈↓a destination that isn't clear or if the object is too heavy.

␈↓ α∧␈↓34)␈↓ αt ␈↓↓∀l s.clear(l,s) ≡ ¬∃x.(¬ab aspect7(x,l,s) ∧ location(x,s) = l)␈↓.

␈↓ α∧␈↓This␈α
says␈α
that␈α
a␈α
location␈α
is␈α
clear␈α
if␈α
there␈α
are␈α
no␈α
objects␈α
there␈α
that␈α
aren't␈α
abnormal␈α
in␈α
␈↓↓aspect7.␈↓␈α
The

␈↓ α∧␈↓ideas␈α
is␈α
to␈αallow␈α
specks␈α
of␈αdust␈α
or␈α
other␈α
trivial␈αobjects.␈α
 However,␈α
the␈αeffect␈α
of␈α
having␈α
␈↓↓ab␈↓␈αunder

␈↓ α∧␈↓the existential quantifier has not yet been evaluated.